/**
 * @file minimize.c
 * @brief a DFA minimization algorithm [need to track down the original source]
 * @author Matthias Stallmann
 * @date 13 February 1992
 * $Id: minimize.c 10 2007-06-28 20:08:57Z mfms $
 */

/*
 *  Copyright (C) 1992, 1994, 2001  Matthias Stallmann.
 *  Contact: matt_stallmann@ncsu.edu
 *
 *  This program is free software; you can redistribute it and/or modify
 *  it under the terms of the GNU General Public License as published by
 *  the Free Software Foundation; either version 2 of the License, or
 *  (at your option) any later version.
 *
 *  This program is distributed in the hope that it will be useful,
 *  but WITHOUT ANY WARRANTY; without even the implied warranty of
 *  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 *  GNU General Public License for more details.
 *
 *  You should have received a copy of the GNU General Public License along
 *  with this program (file COPYING.txt); if not, write to the Free Software
 *  Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301
 *  USA.
 */

/* 2-5-94: BUG DISCOVERED -- the algorithm queues up the name of the
   partition rather than the list of vertices in it;  if the set of
   vertices in a class changes between the time it is put on the queue
   and when it is taken off, some possible refinements are lost.

   Thanks to John Lusth, a student in CSC 522, Spring 1994, for pointing this
   out.

   2-18-94: BUG FIXED -- now the queue stores the list of vertices as
   well as the name of the partition

   28 Nov 2001 - fixed to work with ANSI C compiler
 */

#include <stdio.h>              /* sscanf() */
#include <string.h>             /* strlen(), strcat() */
#include "Gdr.h"
#include "general.h"
#include "alphabet.h"

/* declarations of constants */
#define MAX_PARTITION 100  /* maximum number of equivalence classes */

/* declarations and macros for the animation */
#define MSG_SIZE 1000           /* maximum length of a message */
#define LAB_SIZE 20             /* maximum length of a label */
static char msg[MSG_SIZE];
static TWIN pwin;               /* window for user prompts */
#define XW 5                    /* prompt window coordinates */
#define YW 5
#define init_prompt_window (pwin = create_text_window(XW,YW,""))
#define destroy_prompt_window (kill_window(pwin))

static void wait(char *msg)  /* print msg in prompt window and wait for user */
	           
{
  char *tag;      /* text of common tag to all prompts */
  char *new_msg;  /* to hold msg with tag appended */

  tag = "\nClick RESUME to continue";
  new_msg = (char *)calloc(strlen(msg)+strlen(tag)+1,sizeof(char));
  sprintf(new_msg,"%s%s",msg,tag);
  write_text_window(pwin,new_msg);
  suspend_animation();
  hide_window(pwin);
  free(new_msg);
}
#define COUNT 4

/*    looking for another edge with the same endpoints: */
edge other_edge(vertex v, vertex w) /* returns other edge from v to w if it exists,
                                       NULL_EDGE otherwise */
	            
{
  /* traverse adjacency list of v looking for another edge to w */
  vertex x;  /* other vertex at the end of current edge */
  edge f;    /* current edge */
  for_adjacent(v,f,x) {
    if (x == w) return f;
  }
  return NULL_EDGE;
}

/* data structures: */

/*   accepting versus nonaccepting states.
	     init_states(): make all states non-accepting
		 make_accepting(v): make state v an accepting state
		 make_non_accepting(v): make v a non-accepting state
		 is_accepting(v): returns TRUE if v is an accepting state
*/

static boolean ss[MAX_VERTEX];  /* status of a state (TRUE if accepting) */

void init_states(void)
{
  vertex v;
  for_all_vertices(v) ss[v] = FALSE;
}

#define make_accepting(v) (ss[v] = TRUE)
#define make_non_accepting(v) (ss[v] = FALSE)
#define is_accepting(v) (ss[v])
		 
/*   equivalence classes -- each class is a list of vertices, and each
     class has a unique number, which can be used as an array index.
	NULL_CLASS: a constant representing an invalid class
	init_partition(): put all vertices in the same class and return
	                  the index of that class
	new_partition(): creates a new class and returns its index;
	partition_size(i): returns number of vertices in class with index i
	get_partition(v): returns the index of the class containing vertex v
	get_a_state(i): returns first state in class i
	next_state(v,i): returns next state after v in class i
        change_partition(v,i): move v to class with index i
	for_in_partition(v,i): do the following statement for each v in
	                       class i (only works if v does not change
			       partition) 
        for_all_classes(i): do the following statement for each non-empty
	                    class i (empty classes may arise)
	move_partition(i,j): rename class i to be class j (works only
		             if class j is empty) 
	move_to_front(v): move vertex v to the front of its class list
	reduce(): reduce the graph by picking one representative from
		  each class and redirecting edges so they only go
		  between representatives
*/

typedef int partition;
static vertex fp[MAX_VERTEX];  /* pointer to next vertex in same class */
static vertex bp[MAX_VERTEX];  /* pointer to previous vertex in same class */
static partition vcl[MAX_VERTEX]; /* pointer to class of this vertex */
static vertex cl[MAX_PARTITION]; /* pointer to first vertex in class */
static int ps[MAX_PARTITION];  /* size of class */
static partition max_partition = 0;  /* 1 + index of maximum partition */
#define NULL_CLASS (-1)

partition init_partition(void)
{
  vertex cv,pv;  /* current, previous vertex in list */
  partition new_part;

  new_part = 0;
  max_partition = 1;
  ps[new_part] = 0;  /* initialize size of new class */
  pv = NULL_VERTEX;
  for_all_vertices(cv) {
    if (pv != NULL_VERTEX) fp[pv] = cv;  /* forward link from previous
                                            to current... */
    else cl[new_part] = cv;  /* (or from class header) */
    bp[cv] = pv;  /* and backward link from current to previous */
    vcl[cv] = new_part;  /* make sure cv knows its class */
    ps[new_part]++;  /* update class size */
    pv = cv;
  }
  if (pv != NULL_VERTEX) fp[pv] = NULL_VERTEX; /* last vertex has
                                                  forward link to null */
  else error("Warning: no vertices in graph (init_partition)");
  return(new_part);
}

partition new_partition(void)
{
  partition new_part = max_partition++;

  if (max_partition > MAX_PARTITION) {
    sprintf(err_msg,"Fatal: too many classes, %d (new_partition)",
            max_partition);
    error(err_msg);
    exit(1);
  }
  ps[new_part] = 0;
  cl[new_part] = NULL_VERTEX;
  return(new_part);
}

#define partition_size(i) (ps[i])
#define get_partition(v) (vcl[v])

vertex get_a_state(partition i)
{
  if (ps[i] <= 0 || cl[i] == NULL_VERTEX) {
    sprintf(err_msg,"Fatal: empty class %d %d (get_a_state)",i,ps[i]);
    error(err_msg);
    exit(1);
  }
  return (cl[i]);
}

vertex next_state(vertex v, partition i)
{
  if (vcl[v] != i) {
    sprintf(err_msg,"Fatal: %d not in class %d (next_state)",v,i);
    error(err_msg);
    exit(1);
  }
  return(fp[v]);
}

void change_partition(vertex v, partition new_class)
{
  if (new_class >= max_partition || new_class < 0) {
    sprintf(err_msg,"Fatal: invalid class %d (change_partition)",new_class);
    error(err_msg);
    exit(1);
  }
  
  /* unlink vertex from its current class and decrement size */
  if (bp[v] != NULL_VERTEX) fp[bp[v]] = fp[v];
  else cl[vcl[v]] = fp[v];
  if (fp[v] != NULL_VERTEX) bp[fp[v]] = bp[v];
  ps[vcl[v]]--;

  /* link vertex to the front of new class and increment size */
  fp[v] = cl[new_class];
  if (fp[v] != NULL_VERTEX) bp[fp[v]] = v;
  bp[v] = NULL_VERTEX;
  cl[new_class] = v;
  ps[new_class]++;

  /* change class pointer for vertex */
  vcl[v] = new_class;
}

void move_partition(partition i, partition j)
{
  vertex v;

  if (ps[j] != 0) {
    sprintf(err_msg,"Warning: non-empty partition %d (move_partition)",j);
    error(err_msg);
    return;
  }
  ps[j] = ps[i];
  cl[j] = cl[i];
  ps[i] = 0;
  cl[i] = NULL_VERTEX;
  for(v = cl[j]; v != NULL_VERTEX; v = fp[v]) vcl[v] = j;
}

#define for_in_partition(v,i) for(v = get_a_state(i);\
				  v != NULL_VERTEX;\
				  v = next_state(v,i))
#define for_all_classes(i) for(i = 0; i < max_partition; i++)\
                             if (ps[i] > 0)

void move_to_front(vertex v)
{
  partition i;					/* class for vertex v */
  /* unlink vertex from its current list position */
  if (bp[v] != NULL_VERTEX) fp[bp[v]] = fp[v];
  else cl[vcl[v]] = fp[v];
  if (fp[v] != NULL_VERTEX) bp[fp[v]] = bp[v];

  /* link vertex to the front of its class */
  i = vcl[v];
  fp[v] = cl[i];
  if (fp[v] != NULL_VERTEX) bp[fp[v]] = v;
  bp[v] = NULL_VERTEX;
  cl[i] = v;
}

void reduce(void)
{
  vertex representative[MAX_PARTITION]; /* representative for each class */
  vertex v,w;  /* generic vertices */
  edge e,f;    /* generic edges */
  edge nxt;    /* next edge (for use in loop) */
  vertex v_new,w_new;  /* new endpoints of current edge */
  partition i; /* generic class */
  char *lab;   /* to remember edge label */
  
  wait("About to select a representative for each class");
  
  /* fix up labels for next step */
  for_all_vertices(v) {
    hide_vertex_label(v);
  }
  
  /* select a representative vertex for each partition */
  for_all_classes(i) {
    representative[i] = get_a_state(i);
    expose_vertex_label(representative[i]);
  }
  
  /* give user a chance to look at representatives before completing
     minimization */
  wait("Ready to reduce DFA? (states without labels will be deleted)");
  
  /* adjust edges so that they go between representatives only; keep
     existing edges intact
     
     note: since an edge e may be deleted during its loop iteration, we
     have to be careful to remember its successor on the list before
     deleting it; the macro for_all_edges cannot be used here */
  for(e = first_edge();
      e != NULL_EDGE ? (nxt = next_edge(e), TRUE) : FALSE;
      e = nxt) {
    blink_edge(e,1);
    
    /* compute old and new endpoints of the edge */
    v = tail(e);
    w = head(e);
    v_new = representative[get_partition(v)];
    w_new = representative[get_partition(w)];
    
    /* don't do anything if edge already goes between representatives */
    if ((v == v_new) && (w == w_new)) continue;
    
    /* retrieve the edge label */ 
    lab = edge_label(e);
    
    /* delete the edge */
    delete_edge(e);
    
    /* if there's already an edge between the classes of the two
       endpoints, add to its label if needed; otherwise, create a new
       edge between the two representatives */
    if ((f = other_edge(v_new,w_new)) != NULL_EDGE)
      change_edge_label(f,label_union(edge_label(f),lab));
    else {
      if (v_new == w_new) {
        BEEP;
        sprintf(msg,
                "Loop on vertex %d: click left twice to indicate knots",
                v_new);
        write_text_window(pwin,msg);
        f = add_edge(v_new,w_new,lab);
        hide_window(pwin);
      }
      else f = add_edge(v_new,w_new,lab);
    }
    expose_edge_label(f);
    
    free(lab);
  }
  
  /* delete all non-representative vertices and hide vertex labels */
  for_all_vertices(v) {
    hide_vertex_label(v);
    if (v != representative[get_partition(v)])
      delete_vertex(v);
  }
}

/*   lists of vertices (for queueing the actual list of vertices
     currently in a class, since that list undergoes modification)
	 get_vertex_list(i): make a vertex list consisting of exactly those
	                     vertices in class i and return it
	 for_in_vertex_list(v,L): do what follows for each v in the vertex
	                          list L */

typedef vertex* vertex_list;

vertex_list get_vertex_list(partition i)
{
  vertex v;
  int p;				/* pointer to vertex list */
  vertex_list result;

  result = (vertex_list) calloc(partition_size(i) + 1, sizeof(vertex));
  p = 0;
  for_in_partition(v,i) {
    result[p++] = v;
  }
  result[p] = NULL_VERTEX;
  return result;
}

/* !!! KLUDGE: for this to work, the variable vp must not be otherwise
   defined !!! */
static vertex_list vp;  /* pointer used to traverse the list */
#define for_in_vertex_list(v,L) for(vp = L; (v = *vp) != NULL_VERTEX; vp++)

/*   a list of classes that have been affected in the current iteration
	 along with a marking scheme for affected states
	     init_class_list(): make the list of affected classes empty
         in_class_list(i): TRUE if i is in class list						
		 add_to_class_list(i): add class i to the list of affected classes
         remove_from_class_list(i): reset indicator that shows i is in
                                    the list
		 for_in_class_list(i): do what follows for each class i in the
                        	   list of affected classes
		 mark(v): mark vertex v (and move it to the front of its class list)
         unmark(v): remove mark from vertex v 
         is_marked(v): TRUE if v is marked
         unmarked_vertices(i): TRUE if class i contains unmarked
                               vertices */

static partition class_list[MAX_PARTITION]; /* the class list is an array */
static boolean incl[MAX_PARTITION];  /* TRUE if class is in the list */
static int cl_size = 0;  /* number of items in class list & index of
                            next item to be added to class list */
static boolean mrk[MAX_VERTEX];  /* true if vertex is marked */

void init_class_list(void)
{
  cl_size = 0;
}

#define in_class_list(i) (incl[i])

void add_to_class_list(partition i)
{
  if (incl[i]) return;			/* no need if already in class list */
  if (cl_size >= MAX_PARTITION) {
    sprintf(err_msg,"Fatal: class list full %d (add_to_class_list)",cl_size);
    error(err_msg);
    exit(1);
  }
  class_list[cl_size++] = i;
  incl[i] = TRUE;
}

void remove_from_class_list(partition i)	/* only resets indicator */
	             
{
  incl[i] = FALSE;
}

/* !!! KLUDGE: for this to work, the integer ci must not be otherwise
   defined !!! */
static int ci;  /* index used by the for loop */
#define for_in_class_list(i) for(ci = 0; ci < cl_size\
										 ? (i = class_list[ci],TRUE)\
										 : FALSE; ci++)\
                               if (incl[i])

void mark(vertex v)
{
  mrk[v] = TRUE;
  move_to_front(v);
}

void unmark(vertex v)
{
  mrk[v] = FALSE;
}

#define is_marked(v) (mrk[v])

boolean unmarked_vertices(partition i)
{
  vertex v;

  for_in_partition(v,i) if (!mrk[v]) return(TRUE);
  return(FALSE);
}


/*   a queue of equivalence classes (each entry is a record giving the
     id of the class and its list of vertices when it was queued)
	     empty_queue(): TRUE if queue is empty
	     class_from_queue(): return first class id on the queue
	     list_from_queue(): return first vertex list on the queue
	     delete_queue_front(): delete first record from queue
	     on_queue(i): add a record giving informatin about class i
	                  to the queue
*/

typedef struct { partition entry_class;
  vertex_list entry_vlist; } queue_entry;

static queue_entry queue_array[MAX_PARTITION];  /* the actual queue (as
						   an array) */
static int qfront = 0;  /* index of first item in queue (unless it's empty) */
static int qrear = 0;   /* 1 + index of last item in queue */
static boolean qempty = TRUE;  /* TRUE if queue is empty (qfront == qrear in
                                  this case also) */

#define empty_queue() (qempty)

partition class_from_queue(void)
{
  if (qempty) {
    error("Fatal: queue is empty (off_queue)");
    exit(1);
  }
  return queue_array[qfront].entry_class;
}

vertex_list list_from_queue(void)
{
  if (qempty) {
    error("Fatal: queue is empty (off_queue)");
    exit(1);
  }
  return queue_array[qfront].entry_vlist;
}

partition delete_queue_front(void)
{
  partition item;

  if (qempty) {
    error("Fatal: queue is empty (off_queue)");
    exit(1);
  }
  qfront = (qfront + 1) % MAX_PARTITION;  /* increment qfront mod queue
                                             size */
  if (qfront == qrear) qempty = TRUE;  /* check if queue is now empty */
  return(item);
}

void on_queue(partition i)
{
  if (qfront == qrear && !qempty) {
    sprintf(err_msg,"Fatal: full queue when adding %d (on_queue)",i);
    exit(1);
  }
  queue_array[qrear].entry_class = i;
  queue_array[qrear].entry_vlist = get_vertex_list(i);
  qrear = (qrear + 1) % MAX_PARTITION;  /* increment qrear mod queue size */
  qempty = FALSE;
}


/* macros and functions for handling vertex labels */
/*    showing class of a vertex and whether it is marked: */
void show_status(vertex v)
     /* the state (vertex) */
{
  char lab[LAB_SIZE];

  if (is_marked(v)) sprintf(lab,"%d*",get_partition(v));
  else sprintf(lab,"%d",get_partition(v));
  change_vertex_label(v,lab);
  expose_vertex_label(v);
}

/* the main algorithm */
void minimize(void)
{
  partition accepting,non_accepting;  /* the two initial classes */
  partition current_class;            /* the class used for splitting */
  partition i;                        /* generic class */
  partition mate;		      /* new class split off */
  vertex u,v;                         /* generic vertices */
  vertex nxt;			      /* points to next vertex in class */
  edge e;                             /* generic edge */
  char ch;                            /* generic character */
  
  /* initially, there are two classes, one with accepting states, the
     other with non-accepting states */
  non_accepting = init_partition();
  accepting = new_partition();
  for_all_vertices(v) {
    if (is_accepting(v))
      change_partition(v,accepting);
    show_status(v);
  }
  
  /* put the smaller class on the queue (unless one class is empty); */
  if (partition_size(accepting) > 0 && partition_size(non_accepting) > 0) {
    if (partition_size(accepting) < partition_size(non_accepting)) {
      on_queue(accepting);
    }
    else on_queue(non_accepting);
  }
  
  /* repeatedly use the class at the front of the queue to refine
     the current set of classes; do this until no further changes occur
     (at which point the queue will be empty) */
  while (!empty_queue()) {
    /* get next class to be used as a basis for splitting and
       copy list of vertices in that class (since subsequent
       splits may modify it) */
    vertex_list VL;
    char vl_string[MSG_SIZE];
    current_class = class_from_queue();
    VL = list_from_queue();
    delete_queue_front();
    
    { boolean first_time = TRUE;
    for_in_vertex_list(v,VL) {
      if (first_time) {
        sprintf(vl_string, "%d", v);
        first_time = FALSE;
      }
      else {
        char temp[LAB_SIZE];
        sprintf(temp, ",%d", v);
        strcat(vl_string, temp);
      }
    }
    }
    /* ASSERT: vl_string contains the list VL encoded as a string
       (numbers separated by commas) */

    /* attempt a refinement based on each alphabet symbol */
    for_in_alphabet(ch) {
      /* inform user about class and symbol being considered */
      sprintf(msg, "Refining wrt class %d {%s} and symbol %c",
              current_class, vl_string, ch);
      wait(msg);
      
      /* initialize list of classes affected */
      init_class_list();
      
      /* check incoming edges with label ch for each state in current
         class;
         for each such edge (u,v), mark u and add its class to the list
         of affected classes; note: the mark(u) function automatically
         moves u to the front of its class list */
      for_in_vertex_list(v,VL)
        for_incoming_edges(v,e,u)
        if (is_in_label(ch,edge_label(e))) {
          blink_edge(e,COUNT);
          blink_vertex(u,COUNT);
          mark(u);
          show_status(u);
          add_to_class_list(get_partition(u));
        }
      
      /* if any real splits have occurred, put the smaller of the two
         classes resulting from the split on the queue */
      for_in_class_list(i) {
        if (unmarked_vertices(i)) {
          mate = new_partition();
          sprintf(msg,
                  "New equivalence class %d splits off from %d\n (to %d on symbol %c)",
                  mate,i,current_class,ch);
          wait(msg);
          /* can't use for_in_partition here since v changes class in
             the loop body */
          for(v = get_a_state(i);
              v != NULL_VERTEX ? (nxt = next_state(v,i), TRUE) : FALSE;
              v = nxt) {
            if (!is_marked(v)) break; /* stop at first unmarked vertex */
            change_partition(v,mate);
            unmark(v);
            show_status(v);
          }
	  
          if (partition_size(mate) < partition_size(i))
            on_queue(mate);
          else on_queue(i);
        }
        else { /* all vertices in class i are marked: remove marks */
          sprintf(msg,"No change to class %d",i);
          wait(msg);
          for_in_partition(v,i) {
            unmark(v);
            show_status(v);
          }
        }
        remove_from_class_list(i);
      }
      
    } /* for_in_alphabet */
    free(VL);
  } /* while (!empty_queue()) */
  
  /* reduce the DFA by picking one representative from each class and
     redirecting edges so that they go between representatives;
     non-representative states are deleted */
  reduce();
}

void animat(void)
{
  vertex v;
  
  init_prompt_window;
  
  /* prompt user to draw DFA (or read it in from file) */
  wait("Draw a DFA or read one from a file");
  
  /* compute DFA alphabet (and check that it's deterministic) */
  check_dfa();
  
  /* prompt user to select accepting states (a selected vertex is
     toggled, quit when user types q) */
  write_text_window(pwin,
                    "Select final states:\n - final states are white\n - left click on vertex toggles status of state\n - type `q` to continue");
  while ((v = select_vertex()) != NULL_VERTEX) {
    if (is_highlighted_vertex(v)) {
      un_highlight_vertex(v);
    }
    else {
      highlight_vertex(v);
    }
  }
  hide_window(pwin);

  /* record accepting states */
  for_all_vertices(v) {
    if (is_highlighted_vertex(v)) {
      make_accepting(v);
    }
    else {
      make_non_accepting(v);
    }
  }

  /* encourage user to save DFA before continuing */
  wait("Program destroys DFA;\nRIGHT button -> SAVE to save it in a file");

  /* run minimization algorithm */
  minimize();

  wait("DFA minimization complete; return to edit mode");
  destroy_prompt_window;
}

/*  [Last modified: 2007 06 28 at 19:49:34 GMT] */
